Termination w.r.t. Q proof of TRS/Cimequick.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

test₂(x_0, y) -> True
test₂(x_0, y) -> False
append₂(l1_2, l2_1) -> match_0₃(l1_2, l2_1, l1_2)
match_0₃(l1_2, l2_1, Nil) -> l2_1
match_0₃(l1_2, l2_1, Cons₂(x, l)) -> Cons₂(x, append₂(l, l2_1))
part₂(a_4, l_3) -> match_1₃(a_4, l_3, l_3)
match_1₃(a_4, l_3, Nil) -> Pair₂(Nil, Nil)
match_1₃(a_4, l_3, Cons₂(x, l')) -> match_2₅(x, l', a_4, l_3, part₂(a_4, l'))
match_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> match_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
match_3₇(l1, l2, x, l', a_4, l_3, False) -> Pair₂(Cons₂(x, l1), l2)
match_3₇(l1, l2, x, l', a_4, l_3, True) -> Pair₂(l1, Cons₂(x, l2))
quick₁(l_5) -> match_4₂(l_5, l_5)
match_4₂(l_5, Nil) -> Nil
match_4₂(l_5, Cons₂(a, l')) -> match_5₄(a, l', l_5, part₂(a, l'))
match_5₄(a, l', l_5, Pair₂(l1, l2)) -> append₂(quick₁(l1), Cons₂(a, quick₁(l2)))

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

test₂(x_0, y) -> True
test₂(x_0, y) -> False
append₂(l1_2, l2_1) -> match_0₃(l1_2, l2_1, l1_2)
match_0₃(l1_2, l2_1, Nil) -> l2_1
match_0₃(l1_2, l2_1, Cons₂(x, l)) -> Cons₂(x, append₂(l, l2_1))
part₂(a_4, l_3) -> match_1₃(a_4, l_3, l_3)
match_1₃(a_4, l_3, Nil) -> Pair₂(Nil, Nil)
match_1₃(a_4, l_3, Cons₂(x, l')) -> match_2₅(x, l', a_4, l_3, part₂(a_4, l'))
match_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> match_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
match_3₇(l1, l2, x, l', a_4, l_3, False) -> Pair₂(Cons₂(x, l1), l2)
match_3₇(l1, l2, x, l', a_4, l_3, True) -> Pair₂(l1, Cons₂(x, l2))
quick₁(l_5) -> match_4₂(l_5, l_5)
match_4₂(l_5, Nil) -> Nil
match_4₂(l_5, Cons₂(a, l')) -> match_5₄(a, l', l_5, part₂(a, l'))
match_5₄(a, l', l_5, Pair₂(l1, l2)) -> append₂(quick₁(l1), Cons₂(a, quick₁(l2)))

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

MATCH_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> TEST₂(a_4, x)
MATCH_4₂(l_5, Cons₂(a, l')) -> PART₂(a, l')
APPEND₂(l1_2, l2_1) -> MATCH_0₃(l1_2, l2_1, l1_2)
MATCH_1₃(a_4, l_3, Cons₂(x, l')) -> PART₂(a_4, l')
MATCH_5₄(a, l', l_5, Pair₂(l1, l2)) -> APPEND₂(quick₁(l1), Cons₂(a, quick₁(l2)))
MATCH_5₄(a, l', l_5, Pair₂(l1, l2)) -> QUICK₁(l1)
QUICK₁(l_5) -> MATCH_4₂(l_5, l_5)
MATCH_4₂(l_5, Cons₂(a, l')) -> MATCH_5₄(a, l', l_5, part₂(a, l'))
MATCH_0₃(l1_2, l2_1, Cons₂(x, l)) -> APPEND₂(l, l2_1)
MATCH_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> MATCH_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
MATCH_1₃(a_4, l_3, Cons₂(x, l')) -> MATCH_2₅(x, l', a_4, l_3, part₂(a_4, l'))
PART₂(a_4, l_3) -> MATCH_1₃(a_4, l_3, l_3)
MATCH_5₄(a, l', l_5, Pair₂(l1, l2)) -> QUICK₁(l2)

The TRS R consists of the following rules:

test₂(x_0, y) -> True
test₂(x_0, y) -> False
append₂(l1_2, l2_1) -> match_0₃(l1_2, l2_1, l1_2)
match_0₃(l1_2, l2_1, Nil) -> l2_1
match_0₃(l1_2, l2_1, Cons₂(x, l)) -> Cons₂(x, append₂(l, l2_1))
part₂(a_4, l_3) -> match_1₃(a_4, l_3, l_3)
match_1₃(a_4, l_3, Nil) -> Pair₂(Nil, Nil)
match_1₃(a_4, l_3, Cons₂(x, l')) -> match_2₅(x, l', a_4, l_3, part₂(a_4, l'))
match_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> match_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
match_3₇(l1, l2, x, l', a_4, l_3, False) -> Pair₂(Cons₂(x, l1), l2)
match_3₇(l1, l2, x, l', a_4, l_3, True) -> Pair₂(l1, Cons₂(x, l2))
quick₁(l_5) -> match_4₂(l_5, l_5)
match_4₂(l_5, Nil) -> Nil
match_4₂(l_5, Cons₂(a, l')) -> match_5₄(a, l', l_5, part₂(a, l'))
match_5₄(a, l', l_5, Pair₂(l1, l2)) -> append₂(quick₁(l1), Cons₂(a, quick₁(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

MATCH_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> TEST₂(a_4, x)
MATCH_4₂(l_5, Cons₂(a, l')) -> PART₂(a, l')
APPEND₂(l1_2, l2_1) -> MATCH_0₃(l1_2, l2_1, l1_2)
MATCH_1₃(a_4, l_3, Cons₂(x, l')) -> PART₂(a_4, l')
MATCH_5₄(a, l', l_5, Pair₂(l1, l2)) -> APPEND₂(quick₁(l1), Cons₂(a, quick₁(l2)))
MATCH_5₄(a, l', l_5, Pair₂(l1, l2)) -> QUICK₁(l1)
QUICK₁(l_5) -> MATCH_4₂(l_5, l_5)
MATCH_4₂(l_5, Cons₂(a, l')) -> MATCH_5₄(a, l', l_5, part₂(a, l'))
MATCH_0₃(l1_2, l2_1, Cons₂(x, l)) -> APPEND₂(l, l2_1)
MATCH_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> MATCH_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
MATCH_1₃(a_4, l_3, Cons₂(x, l')) -> MATCH_2₅(x, l', a_4, l_3, part₂(a_4, l'))
PART₂(a_4, l_3) -> MATCH_1₃(a_4, l_3, l_3)
MATCH_5₄(a, l', l_5, Pair₂(l1, l2)) -> QUICK₁(l2)

The TRS R consists of the following rules:

test₂(x_0, y) -> True
test₂(x_0, y) -> False
append₂(l1_2, l2_1) -> match_0₃(l1_2, l2_1, l1_2)
match_0₃(l1_2, l2_1, Nil) -> l2_1
match_0₃(l1_2, l2_1, Cons₂(x, l)) -> Cons₂(x, append₂(l, l2_1))
part₂(a_4, l_3) -> match_1₃(a_4, l_3, l_3)
match_1₃(a_4, l_3, Nil) -> Pair₂(Nil, Nil)
match_1₃(a_4, l_3, Cons₂(x, l')) -> match_2₅(x, l', a_4, l_3, part₂(a_4, l'))
match_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> match_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
match_3₇(l1, l2, x, l', a_4, l_3, False) -> Pair₂(Cons₂(x, l1), l2)
match_3₇(l1, l2, x, l', a_4, l_3, True) -> Pair₂(l1, Cons₂(x, l2))
quick₁(l_5) -> match_4₂(l_5, l_5)
match_4₂(l_5, Nil) -> Nil
match_4₂(l_5, Cons₂(a, l')) -> match_5₄(a, l', l_5, part₂(a, l'))
match_5₄(a, l', l_5, Pair₂(l1, l2)) -> append₂(quick₁(l1), Cons₂(a, quick₁(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 3 SCCs with 5 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

PART₂(a_4, l_3) -> MATCH_1₃(a_4, l_3, l_3)
MATCH_1₃(a_4, l_3, Cons₂(x, l')) -> PART₂(a_4, l')

The TRS R consists of the following rules:

test₂(x_0, y) -> True
test₂(x_0, y) -> False
append₂(l1_2, l2_1) -> match_0₃(l1_2, l2_1, l1_2)
match_0₃(l1_2, l2_1, Nil) -> l2_1
match_0₃(l1_2, l2_1, Cons₂(x, l)) -> Cons₂(x, append₂(l, l2_1))
part₂(a_4, l_3) -> match_1₃(a_4, l_3, l_3)
match_1₃(a_4, l_3, Nil) -> Pair₂(Nil, Nil)
match_1₃(a_4, l_3, Cons₂(x, l')) -> match_2₅(x, l', a_4, l_3, part₂(a_4, l'))
match_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> match_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
match_3₇(l1, l2, x, l', a_4, l_3, False) -> Pair₂(Cons₂(x, l1), l2)
match_3₇(l1, l2, x, l', a_4, l_3, True) -> Pair₂(l1, Cons₂(x, l2))
quick₁(l_5) -> match_4₂(l_5, l_5)
match_4₂(l_5, Nil) -> Nil
match_4₂(l_5, Cons₂(a, l')) -> match_5₄(a, l', l_5, part₂(a, l'))
match_5₄(a, l', l_5, Pair₂(l1, l2)) -> append₂(quick₁(l1), Cons₂(a, quick₁(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

MATCH_1₃(a_4, l_3, Cons₂(x, l')) -> PART₂(a_4, l')

The remaining pairs can at least be oriented weakly.

PART₂(a_4, l_3) -> MATCH_1₃(a_4, l_3, l_3)

Used ordering: Polynomial interpretation [21]:

POL(Cons₂(x₁, x₂)) = 3 + x₂
POL(MATCH_1₃(x₁, x₂, x₃)) = 3 + 3·x₃
POL(PART₂(x₁, x₂)) = 3 + 3·x₂

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ DependencyGraphProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

PART₂(a_4, l_3) -> MATCH_1₃(a_4, l_3, l_3)

The TRS R consists of the following rules:

test₂(x_0, y) -> True
test₂(x_0, y) -> False
append₂(l1_2, l2_1) -> match_0₃(l1_2, l2_1, l1_2)
match_0₃(l1_2, l2_1, Nil) -> l2_1
match_0₃(l1_2, l2_1, Cons₂(x, l)) -> Cons₂(x, append₂(l, l2_1))
part₂(a_4, l_3) -> match_1₃(a_4, l_3, l_3)
match_1₃(a_4, l_3, Nil) -> Pair₂(Nil, Nil)
match_1₃(a_4, l_3, Cons₂(x, l')) -> match_2₅(x, l', a_4, l_3, part₂(a_4, l'))
match_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> match_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
match_3₇(l1, l2, x, l', a_4, l_3, False) -> Pair₂(Cons₂(x, l1), l2)
match_3₇(l1, l2, x, l', a_4, l_3, True) -> Pair₂(l1, Cons₂(x, l2))
quick₁(l_5) -> match_4₂(l_5, l_5)
match_4₂(l_5, Nil) -> Nil
match_4₂(l_5, Cons₂(a, l')) -> match_5₄(a, l', l_5, part₂(a, l'))
match_5₄(a, l', l_5, Pair₂(l1, l2)) -> append₂(quick₁(l1), Cons₂(a, quick₁(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 0 SCCs with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MATCH_0₃(l1_2, l2_1, Cons₂(x, l)) -> APPEND₂(l, l2_1)
APPEND₂(l1_2, l2_1) -> MATCH_0₃(l1_2, l2_1, l1_2)

The TRS R consists of the following rules:

test₂(x_0, y) -> True
test₂(x_0, y) -> False
append₂(l1_2, l2_1) -> match_0₃(l1_2, l2_1, l1_2)
match_0₃(l1_2, l2_1, Nil) -> l2_1
match_0₃(l1_2, l2_1, Cons₂(x, l)) -> Cons₂(x, append₂(l, l2_1))
part₂(a_4, l_3) -> match_1₃(a_4, l_3, l_3)
match_1₃(a_4, l_3, Nil) -> Pair₂(Nil, Nil)
match_1₃(a_4, l_3, Cons₂(x, l')) -> match_2₅(x, l', a_4, l_3, part₂(a_4, l'))
match_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> match_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
match_3₇(l1, l2, x, l', a_4, l_3, False) -> Pair₂(Cons₂(x, l1), l2)
match_3₇(l1, l2, x, l', a_4, l_3, True) -> Pair₂(l1, Cons₂(x, l2))
quick₁(l_5) -> match_4₂(l_5, l_5)
match_4₂(l_5, Nil) -> Nil
match_4₂(l_5, Cons₂(a, l')) -> match_5₄(a, l', l_5, part₂(a, l'))
match_5₄(a, l', l_5, Pair₂(l1, l2)) -> append₂(quick₁(l1), Cons₂(a, quick₁(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

MATCH_0₃(l1_2, l2_1, Cons₂(x, l)) -> APPEND₂(l, l2_1)
APPEND₂(l1_2, l2_1) -> MATCH_0₃(l1_2, l2_1, l1_2)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(APPEND₂(x₁, x₂)) = 2 + 2·x₁
POL(Cons₂(x₁, x₂)) = 1 + x₂
POL(MATCH_0₃(x₁, x₂, x₃)) = 1 + 2·x₃

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

test₂(x_0, y) -> True
test₂(x_0, y) -> False
append₂(l1_2, l2_1) -> match_0₃(l1_2, l2_1, l1_2)
match_0₃(l1_2, l2_1, Nil) -> l2_1
match_0₃(l1_2, l2_1, Cons₂(x, l)) -> Cons₂(x, append₂(l, l2_1))
part₂(a_4, l_3) -> match_1₃(a_4, l_3, l_3)
match_1₃(a_4, l_3, Nil) -> Pair₂(Nil, Nil)
match_1₃(a_4, l_3, Cons₂(x, l')) -> match_2₅(x, l', a_4, l_3, part₂(a_4, l'))
match_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> match_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
match_3₇(l1, l2, x, l', a_4, l_3, False) -> Pair₂(Cons₂(x, l1), l2)
match_3₇(l1, l2, x, l', a_4, l_3, True) -> Pair₂(l1, Cons₂(x, l2))
quick₁(l_5) -> match_4₂(l_5, l_5)
match_4₂(l_5, Nil) -> Nil
match_4₂(l_5, Cons₂(a, l')) -> match_5₄(a, l', l_5, part₂(a, l'))
match_5₄(a, l', l_5, Pair₂(l1, l2)) -> append₂(quick₁(l1), Cons₂(a, quick₁(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

MATCH_4₂(l_5, Cons₂(a, l')) -> MATCH_5₄(a, l', l_5, part₂(a, l'))
QUICK₁(l_5) -> MATCH_4₂(l_5, l_5)
MATCH_5₄(a, l', l_5, Pair₂(l1, l2)) -> QUICK₁(l2)
MATCH_5₄(a, l', l_5, Pair₂(l1, l2)) -> QUICK₁(l1)

The TRS R consists of the following rules:

test₂(x_0, y) -> True
test₂(x_0, y) -> False
append₂(l1_2, l2_1) -> match_0₃(l1_2, l2_1, l1_2)
match_0₃(l1_2, l2_1, Nil) -> l2_1
match_0₃(l1_2, l2_1, Cons₂(x, l)) -> Cons₂(x, append₂(l, l2_1))
part₂(a_4, l_3) -> match_1₃(a_4, l_3, l_3)
match_1₃(a_4, l_3, Nil) -> Pair₂(Nil, Nil)
match_1₃(a_4, l_3, Cons₂(x, l')) -> match_2₅(x, l', a_4, l_3, part₂(a_4, l'))
match_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> match_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
match_3₇(l1, l2, x, l', a_4, l_3, False) -> Pair₂(Cons₂(x, l1), l2)
match_3₇(l1, l2, x, l', a_4, l_3, True) -> Pair₂(l1, Cons₂(x, l2))
quick₁(l_5) -> match_4₂(l_5, l_5)
match_4₂(l_5, Nil) -> Nil
match_4₂(l_5, Cons₂(a, l')) -> match_5₄(a, l', l_5, part₂(a, l'))
match_5₄(a, l', l_5, Pair₂(l1, l2)) -> append₂(quick₁(l1), Cons₂(a, quick₁(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

MATCH_4₂(l_5, Cons₂(a, l')) -> MATCH_5₄(a, l', l_5, part₂(a, l'))
QUICK₁(l_5) -> MATCH_4₂(l_5, l_5)
MATCH_5₄(a, l', l_5, Pair₂(l1, l2)) -> QUICK₁(l2)
MATCH_5₄(a, l', l_5, Pair₂(l1, l2)) -> QUICK₁(l1)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(Cons₂(x₁, x₂)) = 3 + 3·x₂
POL(False) = 2
POL(MATCH_4₂(x₁, x₂)) = 1 + 3·x₂
POL(MATCH_5₄(x₁, x₂, x₃, x₄)) = 3 + 3·x₄
POL(Nil) = 3
POL(Pair₂(x₁, x₂)) = 3 + x₁ + x₂
POL(QUICK₁(x₁)) = 3 + 3·x₁
POL(True) = 3
POL(match_1₃(x₁, x₂, x₃)) = 3·x₃
POL(match_2₅(x₁, x₂, x₃, x₄, x₅)) = 3·x₅
POL(match_3₇(x₁, x₂, x₃, x₄, x₅, x₆, x₇)) = 3 + 3·x₁ + 3·x₂ + 2·x₇
POL(part₂(x₁, x₂)) = 3·x₂
POL(test₂(x₁, x₂)) = 3

The following usable rules [14] were oriented:

match_3₇(l1, l2, x, l', a_4, l_3, True) -> Pair₂(l1, Cons₂(x, l2))
match_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> match_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
test₂(x_0, y) -> False
match_1₃(a_4, l_3, Nil) -> Pair₂(Nil, Nil)
match_3₇(l1, l2, x, l', a_4, l_3, False) -> Pair₂(Cons₂(x, l1), l2)
part₂(a_4, l_3) -> match_1₃(a_4, l_3, l_3)
test₂(x_0, y) -> True
match_1₃(a_4, l_3, Cons₂(x, l')) -> match_2₅(x, l', a_4, l_3, part₂(a_4, l'))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

test₂(x_0, y) -> True
test₂(x_0, y) -> False
append₂(l1_2, l2_1) -> match_0₃(l1_2, l2_1, l1_2)
match_0₃(l1_2, l2_1, Nil) -> l2_1
match_0₃(l1_2, l2_1, Cons₂(x, l)) -> Cons₂(x, append₂(l, l2_1))
part₂(a_4, l_3) -> match_1₃(a_4, l_3, l_3)
match_1₃(a_4, l_3, Nil) -> Pair₂(Nil, Nil)
match_1₃(a_4, l_3, Cons₂(x, l')) -> match_2₅(x, l', a_4, l_3, part₂(a_4, l'))
match_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> match_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
match_3₇(l1, l2, x, l', a_4, l_3, False) -> Pair₂(Cons₂(x, l1), l2)
match_3₇(l1, l2, x, l', a_4, l_3, True) -> Pair₂(l1, Cons₂(x, l2))
quick₁(l_5) -> match_4₂(l_5, l_5)
match_4₂(l_5, Nil) -> Nil
match_4₂(l_5, Cons₂(a, l')) -> match_5₄(a, l', l_5, part₂(a, l'))
match_5₄(a, l', l_5, Pair₂(l1, l2)) -> append₂(quick₁(l1), Cons₂(a, quick₁(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.